a, b:. a  b  0  b - a 

latex

Definitions	T, r - s, , True, t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x), {T}, S  T
Lemmas	mon ident q, qadd inv assoc q, qadd comm q, true wf, squash wf, qadd wf, qmul wf, qadd preserves qle, rationals wf, qsub wf, int inc rationals, qle wf